YES 16.019000000000002 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((divMod :: Int  ->  Int  ->  (Int,Int)) :: Int  ->  Int  ->  (Int,Int))

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\(_,r)→r

is transformed to
r0 (_,r) = r

The following Lambda expression
\qrqr

is transformed to
qr0 qr = qr

The following Lambda expression
\(q,_)→q

is transformed to
q1 (q,_) = q



↳ HASKELL
  ↳ LR
HASKELL
      ↳ IFR

mainModule Main
  ((divMod :: Int  ->  Int  ->  (Int,Int)) :: Int  ->  Int  ->  (Int,Int))

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if signum r == `negate` signum d then (q - 1,r + d) else qr

is transformed to
divMod0 d True = (q - 1,r + d)
divMod0 d False = qr

The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
HASKELL
          ↳ BR

mainModule Main
  ((divMod :: Int  ->  Int  ->  (Int,Int)) :: Int  ->  Int  ->  (Int,Int))

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((divMod :: Int  ->  Int  ->  (Int,Int)) :: Int  ->  Int  ->  (Int,Int))

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
signumReal x
 | x == 0
 = 0
 | x > 0
 = 1
 | otherwise
 = -1

is transformed to
signumReal x = signumReal3 x

signumReal0 x True = -1

signumReal2 x True = 0
signumReal2 x False = signumReal1 x (x > 0)

signumReal1 x True = 1
signumReal1 x False = signumReal0 x otherwise

signumReal3 x = signumReal2 x (x == 0)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  ((divMod :: Int  ->  Int  ->  (Int,Int)) :: Int  ->  Int  ->  (Int,Int))

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
divMod0 d (signum r == `negate` signum d)
where 
divMod0 d True = (q - 1,r + d)
divMod0 d False = qr
q  = q1 vu5
q1 (q,vv) = q
qr  = qr0 vu5
qr0 qr = qr
r  = r0 vu5
r0 (vw,r) = r
vu5  = quotRem n d

are unpacked to the following functions on top level
divModR0 wz xu (vw,r) = r

divModDivMod0 wz xu d True = (divModQ wz xu - 1,divModR wz xu + d)
divModDivMod0 wz xu d False = divModQr wz xu

divModQr0 wz xu qr = qr

divModR wz xu = divModR0 wz xu (divModVu5 wz xu)

divModQ1 wz xu (q,vv) = q

divModVu5 wz xu = quotRem wz xu

divModQr wz xu = divModQr0 wz xu (divModVu5 wz xu)

divModQ wz xu = divModQ1 wz xu (divModVu5 wz xu)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ NumRed

mainModule Main
  ((divMod :: Int  ->  Int  ->  (Int,Int)) :: Int  ->  Int  ->  (Int,Int))

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule Main
  (divMod :: Int  ->  Int  ->  (Int,Int))

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv2721000), Succ(xv950)) → new_primPlusNat(xv2721000, xv950)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(xv2721000), Succ(xv950)) → new_primMinusNat(xv2721000, xv950)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(Succ(xv3000), Zero) → new_primModNatS(Succ(xv3000), Zero, Zero)
new_primModNatS00(xv286, xv287, Succ(xv2880), Succ(xv2890)) → new_primModNatS00(xv286, xv287, xv2880, xv2890)
new_primModNatS1(xv169, xv170) → new_primModNatS0(xv169, xv170)
new_primModNatS01(xv286, xv287) → new_primModNatS(Succ(xv286), Succ(xv287), Succ(xv287))
new_primModNatS0(Succ(xv3000), Succ(xv4000)) → new_primModNatS00(xv3000, xv4000, xv3000, xv4000)
new_primModNatS0(Zero, Zero) → new_primModNatS(Zero, Zero, Zero)
new_primModNatS00(xv286, xv287, Zero, Zero) → new_primModNatS01(xv286, xv287)
new_primModNatS(Succ(xv2910), Succ(xv2920), xv293) → new_primModNatS(xv2910, xv2920, xv293)
new_primModNatS(Succ(xv2910), Zero, xv293) → new_primModNatS1(xv2910, xv293)
new_primModNatS00(xv286, xv287, Succ(xv2880), Zero) → new_primModNatS(Succ(xv286), Succ(xv287), Succ(xv287))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
QDP
                                    ↳ QDPOrderProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(xv286, xv287, Succ(xv2880), Succ(xv2890)) → new_primModNatS00(xv286, xv287, xv2880, xv2890)
new_primModNatS1(xv169, xv170) → new_primModNatS0(xv169, xv170)
new_primModNatS0(Succ(xv3000), Zero) → new_primModNatS(Succ(xv3000), Zero, Zero)
new_primModNatS01(xv286, xv287) → new_primModNatS(Succ(xv286), Succ(xv287), Succ(xv287))
new_primModNatS0(Succ(xv3000), Succ(xv4000)) → new_primModNatS00(xv3000, xv4000, xv3000, xv4000)
new_primModNatS00(xv286, xv287, Zero, Zero) → new_primModNatS01(xv286, xv287)
new_primModNatS(Succ(xv2910), Succ(xv2920), xv293) → new_primModNatS(xv2910, xv2920, xv293)
new_primModNatS(Succ(xv2910), Zero, xv293) → new_primModNatS1(xv2910, xv293)
new_primModNatS00(xv286, xv287, Succ(xv2880), Zero) → new_primModNatS(Succ(xv286), Succ(xv287), Succ(xv287))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primModNatS1(xv169, xv170) → new_primModNatS0(xv169, xv170)
new_primModNatS(Succ(xv2910), Succ(xv2920), xv293) → new_primModNatS(xv2910, xv2920, xv293)
The remaining pairs can at least be oriented weakly.

new_primModNatS00(xv286, xv287, Succ(xv2880), Succ(xv2890)) → new_primModNatS00(xv286, xv287, xv2880, xv2890)
new_primModNatS0(Succ(xv3000), Zero) → new_primModNatS(Succ(xv3000), Zero, Zero)
new_primModNatS01(xv286, xv287) → new_primModNatS(Succ(xv286), Succ(xv287), Succ(xv287))
new_primModNatS0(Succ(xv3000), Succ(xv4000)) → new_primModNatS00(xv3000, xv4000, xv3000, xv4000)
new_primModNatS00(xv286, xv287, Zero, Zero) → new_primModNatS01(xv286, xv287)
new_primModNatS(Succ(xv2910), Zero, xv293) → new_primModNatS1(xv2910, xv293)
new_primModNatS00(xv286, xv287, Succ(xv2880), Zero) → new_primModNatS(Succ(xv286), Succ(xv287), Succ(xv287))
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primModNatS(x1, x2, x3)) = x1   
POL(new_primModNatS0(x1, x2)) = x1   
POL(new_primModNatS00(x1, x2, x3, x4)) = 1 + x1   
POL(new_primModNatS01(x1, x2)) = 1 + x1   
POL(new_primModNatS1(x1, x2)) = 1 + x1   

The following usable rules [17] were oriented: none



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ QDPOrderProof
QDP
                                        ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(Succ(xv3000), Zero) → new_primModNatS(Succ(xv3000), Zero, Zero)
new_primModNatS00(xv286, xv287, Succ(xv2880), Succ(xv2890)) → new_primModNatS00(xv286, xv287, xv2880, xv2890)
new_primModNatS01(xv286, xv287) → new_primModNatS(Succ(xv286), Succ(xv287), Succ(xv287))
new_primModNatS0(Succ(xv3000), Succ(xv4000)) → new_primModNatS00(xv3000, xv4000, xv3000, xv4000)
new_primModNatS00(xv286, xv287, Zero, Zero) → new_primModNatS01(xv286, xv287)
new_primModNatS(Succ(xv2910), Zero, xv293) → new_primModNatS1(xv2910, xv293)
new_primModNatS00(xv286, xv287, Succ(xv2880), Zero) → new_primModNatS(Succ(xv286), Succ(xv287), Succ(xv287))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ QDPOrderProof
                                      ↳ QDP
                                        ↳ DependencyGraphProof
QDP
                                            ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(xv286, xv287, Succ(xv2880), Succ(xv2890)) → new_primModNatS00(xv286, xv287, xv2880, xv2890)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xv312, xv313, Zero, Zero) → new_primDivNatS00(xv312, xv313)
new_primDivNatS0(xv312, xv313, Succ(xv3140), Succ(xv3150)) → new_primDivNatS0(xv312, xv313, xv3140, xv3150)
new_primDivNatS(Succ(xv3170), Zero, xv319) → new_primDivNatS1(xv3170, xv319)
new_primDivNatS(Succ(xv3170), Succ(xv3180), xv319) → new_primDivNatS(xv3170, xv3180, xv319)
new_primDivNatS1(Succ(xv1690), Zero) → new_primDivNatS(Succ(xv1690), Zero, Zero)
new_primDivNatS1(Succ(xv1690), Succ(xv1700)) → new_primDivNatS0(xv1690, xv1700, xv1690, xv1700)
new_primDivNatS00(xv312, xv313) → new_primDivNatS(Succ(xv312), Succ(xv313), Succ(xv313))
new_primDivNatS1(Zero, Zero) → new_primDivNatS(Zero, Zero, Zero)
new_primDivNatS0(xv312, xv313, Succ(xv3140), Zero) → new_primDivNatS(Succ(xv312), Succ(xv313), Succ(xv313))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
QDP
                                    ↳ QDPOrderProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xv312, xv313, Zero, Zero) → new_primDivNatS00(xv312, xv313)
new_primDivNatS0(xv312, xv313, Succ(xv3140), Succ(xv3150)) → new_primDivNatS0(xv312, xv313, xv3140, xv3150)
new_primDivNatS(Succ(xv3170), Zero, xv319) → new_primDivNatS1(xv3170, xv319)
new_primDivNatS(Succ(xv3170), Succ(xv3180), xv319) → new_primDivNatS(xv3170, xv3180, xv319)
new_primDivNatS1(Succ(xv1690), Zero) → new_primDivNatS(Succ(xv1690), Zero, Zero)
new_primDivNatS1(Succ(xv1690), Succ(xv1700)) → new_primDivNatS0(xv1690, xv1700, xv1690, xv1700)
new_primDivNatS00(xv312, xv313) → new_primDivNatS(Succ(xv312), Succ(xv313), Succ(xv313))
new_primDivNatS0(xv312, xv313, Succ(xv3140), Zero) → new_primDivNatS(Succ(xv312), Succ(xv313), Succ(xv313))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primDivNatS(Succ(xv3170), Succ(xv3180), xv319) → new_primDivNatS(xv3170, xv3180, xv319)
new_primDivNatS1(Succ(xv1690), Zero) → new_primDivNatS(Succ(xv1690), Zero, Zero)
new_primDivNatS1(Succ(xv1690), Succ(xv1700)) → new_primDivNatS0(xv1690, xv1700, xv1690, xv1700)
The remaining pairs can at least be oriented weakly.

new_primDivNatS0(xv312, xv313, Zero, Zero) → new_primDivNatS00(xv312, xv313)
new_primDivNatS0(xv312, xv313, Succ(xv3140), Succ(xv3150)) → new_primDivNatS0(xv312, xv313, xv3140, xv3150)
new_primDivNatS(Succ(xv3170), Zero, xv319) → new_primDivNatS1(xv3170, xv319)
new_primDivNatS00(xv312, xv313) → new_primDivNatS(Succ(xv312), Succ(xv313), Succ(xv313))
new_primDivNatS0(xv312, xv313, Succ(xv3140), Zero) → new_primDivNatS(Succ(xv312), Succ(xv313), Succ(xv313))
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2, x3)) = x1   
POL(new_primDivNatS0(x1, x2, x3, x4)) = 1 + x1   
POL(new_primDivNatS00(x1, x2)) = 1 + x1   
POL(new_primDivNatS1(x1, x2)) = 1 + x1   

The following usable rules [17] were oriented: none



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ QDPOrderProof
QDP
                                        ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xv312, xv313, Zero, Zero) → new_primDivNatS00(xv312, xv313)
new_primDivNatS(Succ(xv3170), Zero, xv319) → new_primDivNatS1(xv3170, xv319)
new_primDivNatS0(xv312, xv313, Succ(xv3140), Succ(xv3150)) → new_primDivNatS0(xv312, xv313, xv3140, xv3150)
new_primDivNatS00(xv312, xv313) → new_primDivNatS(Succ(xv312), Succ(xv313), Succ(xv313))
new_primDivNatS0(xv312, xv313, Succ(xv3140), Zero) → new_primDivNatS(Succ(xv312), Succ(xv313), Succ(xv313))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ QDPOrderProof
                                      ↳ QDP
                                        ↳ DependencyGraphProof
QDP
                                            ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(xv312, xv313, Succ(xv3140), Succ(xv3150)) → new_primDivNatS0(xv312, xv313, xv3140, xv3150)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod00(xv141, Zero, Succ(Succ(xv14300)), Zero) → new_divModDivMod00(xv141, Zero, Succ(xv14300), Zero)
new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Zero) → new_divModDivMod00(xv255, xv256, Succ(xv257), xv256)
new_divModDivMod01(xv255, xv256, xv257) → new_divModDivMod00(xv255, xv256, Succ(xv257), xv256)
new_divModDivMod0(xv255, xv256, xv257, Zero, Zero) → new_divModDivMod01(xv255, xv256, xv257)
new_divModDivMod00(xv141, xv142, Succ(xv1430), Succ(xv1440)) → new_divModDivMod00(xv141, xv142, xv1430, xv1440)
new_divModDivMod00(xv141, Succ(xv1420), Succ(Succ(xv14300)), Zero) → new_divModDivMod0(xv141, Succ(xv1420), xv14300, xv14300, xv1420)
new_divModDivMod00(xv141, Zero, Succ(Zero), Zero) → new_divModDivMod00(xv141, Zero, Zero, Zero)
new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Succ(xv2590)) → new_divModDivMod0(xv255, xv256, xv257, xv2580, xv2590)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
QDP
                                      ↳ QDPSizeChangeProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod00(xv141, Zero, Succ(Succ(xv14300)), Zero) → new_divModDivMod00(xv141, Zero, Succ(xv14300), Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
QDP
                                      ↳ QDPOrderProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod01(xv255, xv256, xv257) → new_divModDivMod00(xv255, xv256, Succ(xv257), xv256)
new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Zero) → new_divModDivMod00(xv255, xv256, Succ(xv257), xv256)
new_divModDivMod0(xv255, xv256, xv257, Zero, Zero) → new_divModDivMod01(xv255, xv256, xv257)
new_divModDivMod00(xv141, xv142, Succ(xv1430), Succ(xv1440)) → new_divModDivMod00(xv141, xv142, xv1430, xv1440)
new_divModDivMod00(xv141, Succ(xv1420), Succ(Succ(xv14300)), Zero) → new_divModDivMod0(xv141, Succ(xv1420), xv14300, xv14300, xv1420)
new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Succ(xv2590)) → new_divModDivMod0(xv255, xv256, xv257, xv2580, xv2590)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_divModDivMod00(xv141, xv142, Succ(xv1430), Succ(xv1440)) → new_divModDivMod00(xv141, xv142, xv1430, xv1440)
new_divModDivMod00(xv141, Succ(xv1420), Succ(Succ(xv14300)), Zero) → new_divModDivMod0(xv141, Succ(xv1420), xv14300, xv14300, xv1420)
The remaining pairs can at least be oriented weakly.

new_divModDivMod01(xv255, xv256, xv257) → new_divModDivMod00(xv255, xv256, Succ(xv257), xv256)
new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Zero) → new_divModDivMod00(xv255, xv256, Succ(xv257), xv256)
new_divModDivMod0(xv255, xv256, xv257, Zero, Zero) → new_divModDivMod01(xv255, xv256, xv257)
new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Succ(xv2590)) → new_divModDivMod0(xv255, xv256, xv257, xv2580, xv2590)
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_divModDivMod0(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_divModDivMod00(x1, x2, x3, x4)) = x3   
POL(new_divModDivMod01(x1, x2, x3)) = 1 + x3   

The following usable rules [17] were oriented: none



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
QDP
                                          ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Zero) → new_divModDivMod00(xv255, xv256, Succ(xv257), xv256)
new_divModDivMod01(xv255, xv256, xv257) → new_divModDivMod00(xv255, xv256, Succ(xv257), xv256)
new_divModDivMod0(xv255, xv256, xv257, Zero, Zero) → new_divModDivMod01(xv255, xv256, xv257)
new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Succ(xv2590)) → new_divModDivMod0(xv255, xv256, xv257, xv2580, xv2590)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
                                        ↳ QDP
                                          ↳ DependencyGraphProof
QDP
                                              ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod0(xv255, xv256, xv257, Succ(xv2580), Succ(xv2590)) → new_divModDivMod0(xv255, xv256, xv257, xv2580, xv2590)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod02(xv62, xv63, Succ(xv640), Succ(xv650)) → new_divModDivMod02(xv62, xv63, xv640, xv650)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod04(xv174, Zero, Succ(Succ(xv17600)), Zero) → new_divModDivMod04(xv174, Zero, Succ(xv17600), Zero)
new_divModDivMod04(xv174, Zero, Succ(Zero), Zero) → new_divModDivMod04(xv174, Zero, Zero, Zero)
new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Succ(xv2530)) → new_divModDivMod03(xv249, xv250, xv251, xv2520, xv2530)
new_divModDivMod05(xv249, xv250, xv251) → new_divModDivMod04(xv249, xv250, Succ(xv251), xv250)
new_divModDivMod04(xv174, Succ(xv1750), Succ(Succ(xv17600)), Zero) → new_divModDivMod03(xv174, Succ(xv1750), xv17600, xv17600, xv1750)
new_divModDivMod04(xv174, xv175, Succ(xv1760), Succ(xv1770)) → new_divModDivMod04(xv174, xv175, xv1760, xv1770)
new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Zero) → new_divModDivMod04(xv249, xv250, Succ(xv251), xv250)
new_divModDivMod03(xv249, xv250, xv251, Zero, Zero) → new_divModDivMod05(xv249, xv250, xv251)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
QDP
                                      ↳ QDPSizeChangeProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod04(xv174, Zero, Succ(Succ(xv17600)), Zero) → new_divModDivMod04(xv174, Zero, Succ(xv17600), Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
QDP
                                      ↳ QDPOrderProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod05(xv249, xv250, xv251) → new_divModDivMod04(xv249, xv250, Succ(xv251), xv250)
new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Succ(xv2530)) → new_divModDivMod03(xv249, xv250, xv251, xv2520, xv2530)
new_divModDivMod04(xv174, Succ(xv1750), Succ(Succ(xv17600)), Zero) → new_divModDivMod03(xv174, Succ(xv1750), xv17600, xv17600, xv1750)
new_divModDivMod04(xv174, xv175, Succ(xv1760), Succ(xv1770)) → new_divModDivMod04(xv174, xv175, xv1760, xv1770)
new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Zero) → new_divModDivMod04(xv249, xv250, Succ(xv251), xv250)
new_divModDivMod03(xv249, xv250, xv251, Zero, Zero) → new_divModDivMod05(xv249, xv250, xv251)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_divModDivMod04(xv174, Succ(xv1750), Succ(Succ(xv17600)), Zero) → new_divModDivMod03(xv174, Succ(xv1750), xv17600, xv17600, xv1750)
new_divModDivMod04(xv174, xv175, Succ(xv1760), Succ(xv1770)) → new_divModDivMod04(xv174, xv175, xv1760, xv1770)
The remaining pairs can at least be oriented weakly.

new_divModDivMod05(xv249, xv250, xv251) → new_divModDivMod04(xv249, xv250, Succ(xv251), xv250)
new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Succ(xv2530)) → new_divModDivMod03(xv249, xv250, xv251, xv2520, xv2530)
new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Zero) → new_divModDivMod04(xv249, xv250, Succ(xv251), xv250)
new_divModDivMod03(xv249, xv250, xv251, Zero, Zero) → new_divModDivMod05(xv249, xv250, xv251)
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_divModDivMod03(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_divModDivMod04(x1, x2, x3, x4)) = x3   
POL(new_divModDivMod05(x1, x2, x3)) = 1 + x3   

The following usable rules [17] were oriented: none



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
QDP
                                          ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Succ(xv2530)) → new_divModDivMod03(xv249, xv250, xv251, xv2520, xv2530)
new_divModDivMod05(xv249, xv250, xv251) → new_divModDivMod04(xv249, xv250, Succ(xv251), xv250)
new_divModDivMod03(xv249, xv250, xv251, Zero, Zero) → new_divModDivMod05(xv249, xv250, xv251)
new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Zero) → new_divModDivMod04(xv249, xv250, Succ(xv251), xv250)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
                                        ↳ QDP
                                          ↳ DependencyGraphProof
QDP
                                              ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod03(xv249, xv250, xv251, Succ(xv2520), Succ(xv2530)) → new_divModDivMod03(xv249, xv250, xv251, xv2520, xv2530)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod06(xv94, xv95, Succ(xv960), Succ(xv970)) → new_divModDivMod06(xv94, xv95, xv960, xv970)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Succ(xv2470)) → new_divModDivMod08(xv243, xv244, xv245, xv2460, xv2470)
new_divModDivMod07(xv169, xv170, Succ(xv1710), Succ(xv1720)) → new_divModDivMod07(xv169, xv170, xv1710, xv1720)
new_divModDivMod07(xv169, Zero, Succ(Succ(xv17100)), Zero) → new_divModDivMod07(xv169, Zero, Succ(xv17100), Zero)
new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Zero) → new_divModDivMod07(xv243, xv244, Succ(xv245), xv244)
new_divModDivMod08(xv243, xv244, xv245, Zero, Zero) → new_divModDivMod09(xv243, xv244, xv245)
new_divModDivMod07(xv169, Succ(xv1700), Succ(Succ(xv17100)), Zero) → new_divModDivMod08(xv169, Succ(xv1700), xv17100, xv17100, xv1700)
new_divModDivMod09(xv243, xv244, xv245) → new_divModDivMod07(xv243, xv244, Succ(xv245), xv244)
new_divModDivMod07(xv169, Zero, Succ(Zero), Zero) → new_divModDivMod07(xv169, Zero, Zero, Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
QDP
                                      ↳ QDPSizeChangeProof
                                    ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod07(xv169, Zero, Succ(Succ(xv17100)), Zero) → new_divModDivMod07(xv169, Zero, Succ(xv17100), Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
QDP
                                      ↳ QDPOrderProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Succ(xv2470)) → new_divModDivMod08(xv243, xv244, xv245, xv2460, xv2470)
new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Zero) → new_divModDivMod07(xv243, xv244, Succ(xv245), xv244)
new_divModDivMod07(xv169, xv170, Succ(xv1710), Succ(xv1720)) → new_divModDivMod07(xv169, xv170, xv1710, xv1720)
new_divModDivMod08(xv243, xv244, xv245, Zero, Zero) → new_divModDivMod09(xv243, xv244, xv245)
new_divModDivMod07(xv169, Succ(xv1700), Succ(Succ(xv17100)), Zero) → new_divModDivMod08(xv169, Succ(xv1700), xv17100, xv17100, xv1700)
new_divModDivMod09(xv243, xv244, xv245) → new_divModDivMod07(xv243, xv244, Succ(xv245), xv244)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_divModDivMod07(xv169, xv170, Succ(xv1710), Succ(xv1720)) → new_divModDivMod07(xv169, xv170, xv1710, xv1720)
new_divModDivMod07(xv169, Succ(xv1700), Succ(Succ(xv17100)), Zero) → new_divModDivMod08(xv169, Succ(xv1700), xv17100, xv17100, xv1700)
The remaining pairs can at least be oriented weakly.

new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Succ(xv2470)) → new_divModDivMod08(xv243, xv244, xv245, xv2460, xv2470)
new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Zero) → new_divModDivMod07(xv243, xv244, Succ(xv245), xv244)
new_divModDivMod08(xv243, xv244, xv245, Zero, Zero) → new_divModDivMod09(xv243, xv244, xv245)
new_divModDivMod09(xv243, xv244, xv245) → new_divModDivMod07(xv243, xv244, Succ(xv245), xv244)
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_divModDivMod07(x1, x2, x3, x4)) = x3   
POL(new_divModDivMod08(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_divModDivMod09(x1, x2, x3)) = 1 + x3   

The following usable rules [17] were oriented: none



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
QDP
                                          ↳ DependencyGraphProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Succ(xv2470)) → new_divModDivMod08(xv243, xv244, xv245, xv2460, xv2470)
new_divModDivMod08(xv243, xv244, xv245, Zero, Zero) → new_divModDivMod09(xv243, xv244, xv245)
new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Zero) → new_divModDivMod07(xv243, xv244, Succ(xv245), xv244)
new_divModDivMod09(xv243, xv244, xv245) → new_divModDivMod07(xv243, xv244, Succ(xv245), xv244)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
                                        ↳ QDP
                                          ↳ DependencyGraphProof
QDP
                                              ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod08(xv243, xv244, xv245, Succ(xv2460), Succ(xv2470)) → new_divModDivMod08(xv243, xv244, xv245, xv2460, xv2470)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_divModDivMod010(xv89, xv90, Succ(xv910), Succ(xv920)) → new_divModDivMod010(xv89, xv90, xv910, xv920)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: